#include "cnf2aig/cnfToAig.h"
#include "ParseUtils.h"
#include "base/aig.h"

using QuteRSAT::AigIndex;
using QuteRSAT::AigCircuit;
using QuteRSAT::CnfToAig;

template<class B, class Solver>
static void readClause(B& in, Solver& S, vector<uint32_t>& lits) {
    int     parsed_lit, var;
    lits.clear();
    for (;;){
        parsed_lit = parseInt(in);
        if (parsed_lit == 0) break;
        var = abs(parsed_lit);
//        assert( var < S.nVars() );
        lits.push_back( var << 1 | (parsed_lit > 0) );
//        lits.push( (parsed_lit > 0) ? Lit(var) : ~Lit(var) );
    }
}

template<class B>
static unsigned parse_header( B & in)
{
   int vars    = 0;
   int clauses = 0;
   for (;;){
       skipWhitespace(in);
       if (*in == 'p'){
          if (eagerMatch(in, "p cnf")){
             vars    = parseInt(in);
             clauses = parseInt(in);
             break;
          }
          else{
             printf("PARSE ERROR! Unexpected char: %c\n", *in), exit(3);
          }
       }
       else if (*in == 'c' || *in == 'p')
          skipLine(in);
   }
   return vars;
}

template<class B, class Solver>
static void parse_DIMACS(B& in, Solver& S) {
    vector<uint32_t> lits;
    int cnt     = 0;
    for (;;){
        skipWhitespace(in);
        if (*in == EOF) break;
        else if (*in == 'c' || *in == 'p')
            skipLine(in);
        else{
            cnt++;
            readClause(in, S, lits);
            S.addClause(lits); }
    }
}

int main( unsigned argc , const char ** argv )
{
   if( argc != 3 )exit(1);
   vector<AigIndex> link;
   AigCircuit ckt;
   
   gzFile f = (argc == 1) ? gzdopen(0, "rb") : gzopen(argv[1], "rb");
   StreamBuffer in(f);
   unsigned var = parse_header( in )+1; 
   CnfToAig tran( var , ckt, link );
   parse_DIMACS( in , tran );
   gzclose( f );
   tran.run(); 
   if( tran.isUnSat() ) 
   {
      cout << "UNSAT" <<endl;
      exit( 1 ) ;
   }
   cout << tran.getCoverRate() << endl;

   StrashAIG nckt;
   ckt.transform( nckt , link );
   nckt.write_aig( argv[2] );
}
